Theory Incredible_Propositional_Tasks

theory Incredible_Propositional_Tasks
imports
  Incredible_Completeness
  Incredible_Propositional
begin

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

subsubsection Task 1.1

text This is the very first task of the Incredible Proof Machine: @{term "A  A"}

abbreviation A :: "(string,prop_funs) pform"
  where "A  Fun (Const ''A'') []"

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

interpretation task1_1: Abstract_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[A]"
  "[A]"
by unfold_locales simp

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

lemma "task1_1.solved"
  unfolding task1_1.solved_def
apply clarsimp
apply (rule_tac x="{|A|}" in exI)
apply clarsimp
apply (rule_tac x="Node ({|A|}  A, Axiom) {||}" in exI)
apply clarsimp
apply (rule conjI)
 apply (rule task1_1.wf)
   apply (solves clarsimp)
  apply clarsimp
  apply (rule task1_1.eff.intros(1))
  apply (solves simp)
 apply (solves clarsimp)
by (auto intro: tfinite.intros)


print_locale Vertex_Graph
interpretation task1_1: Vertex_Graph task1_1.nodes task1_1.inPorts task1_1.outPorts "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
.

print_locale Pre_Port_Graph
interpretation task1_1: Pre_Port_Graph task1_1.nodes task1_1.inPorts task1_1.outPorts "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  "{((0,Reg A),(1,plain_ant A))}"
.

print_locale Instantiation
interpretation task1_1: Instantiation
  task1_1.inPorts
  task1_1.outPorts
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  task1_1.hyps
  task1_1.nodes
  "{((0,Reg A),(1,plain_ant A))}"
  "{|0::nat,1|}"
  task1_1.labelsIn
  task1_1.labelsOut
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  "id"
  "undefined"
by unfold_locales simp

declare One_nat_def [simp del]

lemma path_one_edge[simp]:
  "task1_1.path v1 v2 pth 
    (v1 = 0  v2 = 1  pth = [((0,Reg A),(1,plain_ant A))] 
    pth = []  v1 = v2)"
  apply (cases pth)
  apply (auto simp add: task1_1.path_cons_simp')
  apply (rename_tac list, case_tac list, auto simp add: task1_1.path_cons_simp')+
  done

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

interpretation Tasked_Proof_Graph
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[A]"
  "[A]"
  "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  "{((0,Reg A),(1,plain_ant A))}"
  "id"
  "undefined"
apply unfold_locales
        apply (solves simp)
       apply (solves clarsimp)
      apply (solves clarsimp)
     apply (solves clarsimp)
    apply (solves fastforce)
   apply (solves fastforce)
  apply (solves clarsimp simp add: task1_1.labelAtOut_def task1_1.labelAtIn_def)
 apply (solves clarsimp)
apply (solves clarsimp)
done

subsubsection Task 2.11

text This is a slightly more interesting task as it involves both our connectives: @{term "P  Q  R  P  (Q  R)"}

abbreviation B :: "(string,prop_funs) pform"
  where "B  Fun (Const ''B'') []"
abbreviation C :: "(string,prop_funs) pform"
  where "C  Fun (Const ''C'') []"

interpretation task2_11: Abstract_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[Fun imp [Fun and [A,B],C]]"
  "[Fun imp [A,Fun imp [B,C]]]"
by unfold_locales simp_all

abbreviation "n_andI  task2_11.n_rules !! 0"
abbreviation "n_andE1  task2_11.n_rules !! 1"
abbreviation "n_andE2  task2_11.n_rules !! 2"
abbreviation "n_impI  task2_11.n_rules !! 3"
abbreviation "n_impE  task2_11.n_rules !! 4"

lemma n_andI [simp]: "n_andI = (andI, Fun and [X,Y])"
  unfolding task2_11.n_rules_def by (simp add: prop_rules_def)
lemma n_andE1 [simp]: "n_andE1 = (andE, X)"
  unfolding task2_11.n_rules_def One_nat_def by (simp add: prop_rules_def)
lemma n_andE2 [simp]: "n_andE2 = (andE, Y)"
  unfolding task2_11.n_rules_def numeral_2_eq_2 by (simp add: prop_rules_def)
lemma n_impI [simp]: "n_impI = (impI, Fun imp [X,Y])"
  unfolding task2_11.n_rules_def numeral_3_eq_3 by (simp add: prop_rules_def)
lemma n_impE [simp]: "n_impE = (impE, Y)"
proof -
  have "n_impE = task2_11.n_rules !! Suc 3" by simp
  also have "... = (impE, Y)"
  unfolding task2_11.n_rules_def numeral_3_eq_3 by (simp add: prop_rules_def)
  finally show ?thesis .
qed


lemma subst_Var_eq_id [simp]: "subst Var = id"
  by (rule ext) (induct_tac x; auto simp: map_idI)

lemma xy_update: "f = undefined(''X'' := x, ''Y'' := y)  x = f ''X''  y = f ''Y''" by force
lemma y_update: "f = undefined(''Y'':=y)  y = f ''Y''" by force

declare snth.simps(1) [simp del]

text By interpreting @{term Solved_Task} we show that there is a proof tree for the task.
  We get the existence of the proof graph for free by using the completeness theorem.

interpretation task2_11: Solved_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[Fun imp [Fun and [A,B],C]]"
  "[Fun imp [A,Fun imp [B,C]]]"
apply unfold_locales
  unfolding task2_11.solved_def
apply clarsimp
apply (rule_tac x="{|Fun imp [Fun and [A,B],C]|}" in exI)
apply clarsimp
― ‹The actual proof tree for this task.
apply (rule_tac x="Node ({|Fun imp [Fun and [A, B], C]|}  Fun imp [A, Fun imp [B, C]],NatRule n_impI)
  {|Node ({|Fun imp [Fun and [A, B], C], A|}  Fun imp [B,C],NatRule n_impI)
    {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  C,NatRule n_impE)
      {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  Fun imp [Fun and [A,B], C],Axiom) {||},
        Node ({|Fun imp [Fun and [A, B], C], A, B|}  Fun and [A,B],NatRule n_andI) 
          {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  A,Axiom) {||},
            Node ({|Fun imp [Fun and [A, B], C], A, B|}  B,Axiom) {||}
          |}
      |}
    |}
  |}" in exI)
apply clarsimp
apply (rule conjI)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impI snth_smap snth_sset)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (intro conjI; simp; rule xy_update)
   apply (solves simp)
  apply (solves fastforce simp: propositional.f_antecedent_def)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impI snth_smap snth_sset)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (intro conjI; simp; rule xy_update)
   apply (solves simp)
  apply (solves fastforce simp: propositional.f_antecedent_def)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impE snth_smap snth_sset)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified, where s="undefined(''Y'':=C,''X'':=Fun and [A,B])"]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (solves intro conjI; simp)
  apply (solves simp add: propositional.f_antecedent_def)
 apply (erule disjE)

  apply (auto intro: task1_1.wf intro!: task1_1.eff.intros(1))[1]

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_andI snth_smap snth_sset)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (intro conjI; simp; rule xy_update)
   apply (solves simp)
  apply (solves simp add: propositional.f_antecedent_def)
 apply clarsimp

 apply (erule disjE)
  apply (solves rule task1_1.wf; auto intro: task1_1.eff.intros(1))
 apply (solves rule task1_1.wf; auto intro: task1_1.eff.intros(1))
  
by (rule tfinite.intros; auto)+


interpretation Tasked_Proof_Graph
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[Fun imp [Fun and [A,B],C]]"
  "[Fun imp [A,Fun imp [B,C]]]"
  task2_11.vertices 
  task2_11.nodeOf 
  task2_11.edges
  task2_11.vidx
  task2_11.inst
by unfold_locales

end

end