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))"

context Abstract_Task
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.›

locale Tasked_Proof_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