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