# Theory Abstract_Rules_To_Incredible

```theory Abstract_Rules_To_Incredible
imports
Main
"HOL-Library.FSet"
"HOL-Library.Stream"
Incredible_Deduction
Abstract_Rules
begin

text ‹In this theory, the abstract rules given in @{theory Incredible_Proof_Machine.Abstract_Rules} are used to
create a proper signature.›

text ‹Besides the rules given there, we have nodes for assumptions, conclusions, and the helper
block.›

datatype ('form, 'rule) graph_node = Assumption 'form | Conclusion 'form | Rule 'rule | Helper

type_synonym ('form, 'var) in_port = "('form, 'var) antecedent"
type_synonym 'form reg_out_port = "'form"
type_synonym 'form hyp = "'form"
datatype ('form, 'var) out_port = Reg "'form reg_out_port" | Hyp "'form hyp" "('form, 'var) in_port"
type_synonym ('v, 'form, 'var) edge' = "(('v × ('form, 'var) out_port) × ('v × ('form, 'var) in_port))"

begin
definition nodes :: "('form, 'rule) graph_node stream" where
"nodes = Helper ## shift (map Assumption assumptions) (shift (map Conclusion conclusions) (smap Rule rules))"

lemma Helper_in_nodes[simp]:
"Helper ∈ sset nodes" by (simp add: nodes_def)
lemma Assumption_in_nodes[simp]:
"Assumption a ∈ sset nodes ⟷ a ∈ set assumptions" by (auto simp add: nodes_def stream.set_map)
lemma Conclusion_in_nodes[simp]:
"Conclusion c ∈ sset nodes ⟷ c ∈ set conclusions" by (auto simp add: nodes_def stream.set_map)
lemma Rule_in_nodes[simp]:
"Rule r ∈ sset nodes ⟷ r ∈ sset rules" by (auto simp add: nodes_def stream.set_map)

fun inPorts' :: "('form, 'rule) graph_node ⇒ ('form, 'var) in_port list"  where
"inPorts' (Rule r) = antecedent r"
|"inPorts' (Assumption r) = []"
|"inPorts' (Conclusion r) = [ plain_ant r ]"
|"inPorts' Helper  = [ plain_ant anyP ]"

fun inPorts :: "('form, 'rule) graph_node ⇒ ('form, 'var) in_port fset"  where
"inPorts (Rule r) = f_antecedent r"
|"inPorts (Assumption r) = {||}"
|"inPorts (Conclusion r) = {| plain_ant r |}"
|"inPorts Helper  = {| plain_ant anyP |}"

lemma inPorts_fset_of:
"inPorts n = fset_from_list (inPorts' n)"
by (cases n rule: inPorts.cases) (auto simp: f_antecedent_def)

definition outPortsRule where
"outPortsRule r = ffUnion ((λ a. (λ h. Hyp h a) |`| a_hyps a) |`| f_antecedent r) |∪| Reg |`| f_consequent r"

lemma Reg_in_outPortsRule[simp]:  "Reg c |∈| outPortsRule r ⟷ c |∈| f_consequent r"
by (auto simp add: outPortsRule_def ffUnion.rep_eq)
lemma Hyp_in_outPortsRule[simp]:  "Hyp h c |∈| outPortsRule r ⟷ c |∈| f_antecedent r ∧ h |∈| a_hyps c"
by (auto simp add: outPortsRule_def ffUnion.rep_eq)

fun outPorts where
"outPorts (Rule r) = outPortsRule r"
|"outPorts (Assumption r) = {|Reg r|}"
|"outPorts (Conclusion r) = {||}"
|"outPorts Helper  = {| Reg anyP |}"

fun labelsIn where
"labelsIn _ p = a_conc p"

fun labelsOut where
"labelsOut _ (Reg p) = p"
| "labelsOut _ (Hyp h c) = h"

fun hyps where
"hyps (Rule r) (Hyp h a) = (if a |∈| f_antecedent r ∧ h |∈| a_hyps a then Some a else None)"
| "hyps _ _ = None"

fun local_vars :: "('form, 'rule) graph_node ⇒ ('form, 'var) in_port ⇒ 'var set"  where
"local_vars _ a = a_fresh a"

sublocale Labeled_Signature nodes inPorts outPorts hyps labelsIn labelsOut
proof(standard,goal_cases)
case (1 n p1 p2)
thus ?case by(induction n p1 rule: hyps.induct) (auto  split: if_splits)
qed

lemma hyps_for_conclusion[simp]: "hyps_for (Conclusion n) p = {||}"
using hyps_for_subset by auto
lemma hyps_for_Helper[simp]: "hyps_for Helper p = {||}"
using hyps_for_subset by auto
lemma hyps_for_Rule[simp]: "ip |∈| f_antecedent r ⟹ hyps_for (Rule r) ip = (λ h. Hyp h ip) |`| a_hyps ip"
by (auto elim!: hyps.elims split: if_splits)
end

text ‹Finally, a given proof graph solves the task at hand if all the given conclusions are present
as conclusion blocks in the graph.›

Abstract_Task freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP  antecedent consequent rules assumptions conclusions  +
Scoped_Proof_Graph freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP  inPorts outPorts nodeOf hyps nodes vertices labelsIn labelsOut vidx inst edges local_vars
for freshenLC :: "nat ⇒ 'var ⇒ 'var"
and renameLCs :: "('var ⇒ 'var) ⇒ 'form ⇒ 'form"
and lconsts :: "'form ⇒ 'var set"
and closed :: "'form ⇒ bool"
and subst :: "'subst ⇒ 'form ⇒ 'form"
and subst_lconsts :: "'subst ⇒ 'var set"
and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
and anyP :: "'form"

and antecedent :: "'rule ⇒ ('form, 'var) antecedent list"
and consequent :: "'rule ⇒ 'form list"
and rules :: "'rule stream"

and assumptions :: "'form list"
and conclusions :: "'form list"

and vertices :: "'vertex fset"
and nodeOf :: "'vertex ⇒ ('form, 'rule) graph_node"
and edges :: "('vertex, 'form, 'var) edge' set"
and vidx :: "'vertex ⇒ nat"
and inst :: "'vertex ⇒ 'subst"  +
assumes conclusions_present: "set (map Conclusion conclusions) ⊆ nodeOf ` fset vertices"

end
```