Theory Incredible_Predicate_Tasks

theory Incredible_Predicate_Tasks
imports
  Incredible_Completeness
  Incredible_Predicate
  "HOL-Eisbach.Eisbach"
begin

declare One_nat_def [simp del]

context ND_Rules_Inst begin
lemma eff_NatRuleI:
  "nat_rule rule c ants
     entail = (Γ  subst s (freshen a c))
     hyps = ((λant. ((λp. subst s (freshen a p)) |`| a_hyps ant |∪| Γ  subst s (freshen a (a_conc ant)))) |`| ants)
     ( ant f. ant |∈| ants  f |∈| Γ  freshenLC a ` (a_fresh ant)  lconsts f = {})
     ( ant. ant |∈| ants  freshenLC a ` (a_fresh ant)  subst_lconsts s = {})
     eff (NatRule rule) entail hyps"
  by (drule eff.intros(2)) simp_all
end

context Abstract_Task begin
lemma  natEff_InstI:
  "rule = (r,c)
   c  set (consequent r)
   antec = f_antecedent r
   natEff_Inst rule c antec"
  by (metis natEff_Inst.intros)
end

context begin

text A typical task with local constants:: ∀x. Q x ⟶ Q x›

text First the task is defined as an @{term Abstract_Task}.

interpretation task: Abstract_Task
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  antecedent
  consequent
  prop_rules
  "[]"
  "[ForallX (imp (Q x) (Q x))]"
by unfold_locales auto

text Then we show, that this task has a proof within our formalization of natural deduction
  by giving a concrete proof tree.

abbreviation lx :: "nat" where "lx  to_nat (1::nat,0::nat)"

abbreviation base_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
  "base_tree  Node ({|Q (LC lx)|}  Q (LC lx), Axiom) {||}"

abbreviation imp_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
  "imp_tree  Node ({||}  imp (Q (LC lx)) (Q (LC lx)), NatRule (impI, imp X Y)) {|base_tree|}"

abbreviation solution_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
  "solution_tree  Node ({||}  ForallX (imp (Q x) (Q x)), NatRule (allI, ForallX (P x))) {|imp_tree|}"

abbreviation s1 where "s1  [(12, ([9], imp (Q x) (Q x)))] "
abbreviation s2 where "s2  [(10, ([], Q (LC lx))), (11, ([], Q (LC lx)))] "

lemma fv_subst_s1[simp]: "fv_subst s1 = {}"
  by (simp add: fv_subst_def)

lemma subst1_simps[simp]:
  "subst s1 (P (LC n)) = imp (Q (LC n)) (Q (LC n))"
  "subst s1 (ForallX (P x)) = ForallX (imp (Q x) (Q x))"
  by simp_all

lemma subst2_simps[simp]:
    "subst s2 X = Q (LC lx)" 
    "subst s2 Y = Q (LC lx)"
    "subst s2 (imp X Y) = imp (subst s2 X) (subst s2 Y)"
  by simp_all

lemma substI1: "ForallX (imp (Q x) (Q x)) = subst s1 (predicate.freshen 1 (ForallX (P x)))"
  by (auto simp add: predicate.freshen_def Let_def)

lemma substI2: "imp (Q (LC lx)) (Q (LC lx)) = subst s2 (predicate.freshen 2 (imp X Y))"
  by (auto simp add: predicate.freshen_def Let_def)

declare subst.simps[simp del]

lemma "task.solved"
  unfolding task.solved_def
apply clarsimp
apply (rule_tac x="{||}" in exI)
apply clarsimp
apply (rule_tac x="solution_tree" in exI)
apply clarsimp
apply (rule conjI)

 apply (rule task.wf)
   apply (solves (auto simp add: stream.set_map task.n_rules_def)[1])
  apply clarsimp
  apply (rule task.eff_NatRuleI)
      apply (solves rule task.natEff_Inst.intros;simp)
     apply clarsimp     
     apply (rule conjI)
      apply (solves simp)
     apply (solves rule substI1)
    apply (simp add: predicate.f_antecedent_def predicate.freshen_def)
    apply (subst antecedent.sel(2))
    apply (solves simp)
   apply (solves simp)
  apply (solves simp)
 apply simp

 apply (rule task.wf)
   apply (solves (auto simp add: stream.set_map task.n_rules_def)[1])
  apply clarsimp
  apply (rule task.eff_NatRuleI)
      apply (solves rule task.natEff_Inst.intros; simp)
     apply clarsimp     
     apply (rule conjI)
      apply (solves simp)
     apply (solves rule substI2)
    apply (solves simp add: predicate.f_antecedent_def predicate.freshen_def)
   apply (solves simp)
  apply (solves simp add: predicate.f_antecedent_def)
 apply simp

 apply (solves (auto intro: task.wf intro!: task.eff.intros(1))[1])
apply (solves (rule tfinite.intros, simp)+)
done

abbreviation vertices where "vertices  {|0::nat,1,2 |}"
fun nodeOf  where 
    "nodeOf n = [Conclusion (ForallX (imp (Q x) (Q x))), 
                 Rule allI, 
                 Rule impI] ! n "

fun inst  where 
    "inst n = [[],s1,s2] ! n"


interpretation task: Vertex_Graph task.nodes task.inPorts task.outPorts vertices nodeOf.

abbreviation e1 :: "(nat, form, nat) edge'"
  where "e1  ((1,Reg (ForallX (P x))), (0,plain_ant (ForallX (imp (Q x) (Q x)))))"
abbreviation e2  :: "(nat, form, nat) edge'"
  where "e2  ((2,Reg (imp X Y)), (1,allI_input))"
abbreviation e3  :: "(nat, form, nat) edge'"
  where "e3  ((2,Hyp X (impI_input)), (2,impI_input))"
abbreviation task_edges :: "(nat, form, nat) edge' set" where "task_edges  {e1, e2, e3}"


interpretation task: Scoped_Graph task.nodes task.inPorts task.outPorts vertices nodeOf task_edges task.hyps
  by standard (auto simp add: predicate.f_consequent_def predicate.f_antecedent_def)

interpretation task: Instantiation
  task.inPorts
  task.outPorts
  nodeOf
  task.hyps
  task.nodes
  task_edges
  vertices
  task.labelsIn
  task.labelsOut
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  "id"
  "inst"
by unfold_locales simp

text Finally we can also show that there is a proof graph for this task.

interpretation Well_Scoped_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf
  task_edges
  task.hyps
by standard (auto split: if_splits)

lemma no_path_01[simp]: "task.path 0 v pth  (pth = []  v = 0)"
  by (cases pth) (auto simp add: task.path_cons_simp)
lemma no_path_12[simp]: "¬ task.path 1 2 pth"
  by (cases pth) (auto simp add: task.path_cons_simp)

interpretation Acyclic_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf
  task_edges
  task.hyps
proof
  fix v pth 
  assume "task.path v v pth" and "task.hyps_free pth"
  thus "pth = []"
    by (cases pth) (auto simp add: task.path_cons_simp predicate.f_antecedent_def)
qed

interpretation Saturated_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf
  task_edges
by standard
   (auto simp add: predicate.f_consequent_def predicate.f_antecedent_def) 

interpretation Pruned_Port_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf
  task_edges
proof
  fix v
  assume "v |∈| vertices"
  hence " pth. task.path v 0 pth"
    apply auto
    apply (rule exI[where x = "[e1]"], auto simp add: task.path_cons_simp)
    apply (rule exI[where x = "[e2,e1]"], auto simp add: task.path_cons_simp)
    done
  moreover
  have "task.terminal_vertex 0" by auto
  ultimately
  show "pth v'. task.path v v' pth  task.terminal_vertex v'" by blast
qed

interpretation Well_Shaped_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf task_edges
  task.hyps
..

interpretation Solution
  task.inPorts
  task.outPorts
  nodeOf
  task.hyps
  task.nodes
  vertices
  task.labelsIn
  task.labelsOut
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  id
  inst
  task_edges
by standard
   (auto simp add: task.labelAtOut_def task.labelAtIn_def predicate.freshen_def, subst antecedent.sel, simp)

interpretation Proof_Graph
  task.nodes
  task.inPorts
  task.outPorts
  vertices
  nodeOf
  task_edges
  task.hyps
  task.labelsIn
  task.labelsOut
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  id
  inst
..

lemma path_20:
  assumes "task.path 2 0 pth"
  shows "(1, allI_input)  snd ` set pth"
proof-
  { fix v
    assume "task.path v 0 pth"
    hence "v = 0  v = 1  (1, allI_input)  snd ` set pth"
    by (induction v "0::nat" pth rule: task.path.induct) auto
  }
  from this[OF assms]
  show ?thesis by auto
qed

lemma scope_21: "2  task.scope (1, allI_input)"
  by (auto intro!: task.scope.intros elim: path_20 simp add: task.outPortsRule_def predicate.f_antecedent_def predicate.f_consequent_def)

interpretation Scoped_Proof_Graph
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  task.inPorts
  task.outPorts
  nodeOf
  task.hyps
  task.nodes
  vertices
  task.labelsIn
  task.labelsOut
  id
  inst
  task_edges
  task.local_vars
by standard (auto simp add: predicate.f_antecedent_def scope_21)

interpretation Tasked_Proof_Graph
  "curry to_nat :: nat  var  var"
  map_lc
  lc
  "closed"
  subst
  lc_subst
  map_lc_subst
  "Var 0 []"
  antecedent
  consequent
  prop_rules
  "[]"
  "[ForallX (imp (Q x) (Q x))]"
  vertices
  nodeOf
  task_edges
  id
  inst
by unfold_locales auto

end

end