Theory Case_Labeling

theory Case_Labeling
imports Main
keywords "print_nested_cases" :: diag
begin

section ‹Labeling Subgoals›

context begin
  qualified type_synonym prg_ctxt_var = unit
  qualified type_synonym prg_ctxt = "string × nat × prg_ctxt_var list"
  
  text ‹Embed variables in terms›
  qualified definition VAR :: "'v ⇒ prg_ctxt_var" where
    "VAR _ = ()"
  
  text ‹Labeling of a subgoal›
  qualified definition VC :: "prg_ctxt list ⇒ 'a ⇒ 'a" where
    "VC ct P ≡ P"
  
  text ‹Computing the statement numbers and context›
  qualified definition CTXT :: "nat ⇒ prg_ctxt list ⇒ nat ⇒ 'a ⇒ 'a" where
    "CTXT inp ct outp P ≡ P"
  
  text ‹Labeling of a term binding or assumption›
  qualified definition BIND :: "string ⇒ nat ⇒ 'a ⇒ 'a" where
    "BIND name inp P ≡ P"

  text ‹Hierarchy labeling›
  qualified definition HIER :: "prg_ctxt list ⇒ 'a ⇒ 'a" where
    "HIER ct P ≡ P"

  text ‹Split Labeling. This is used as an assumption›
  qualified definition SPLIT :: "'a ⇒ 'a ⇒ bool" where
    "SPLIT v w ≡ v = w"

  text ‹Disambiguation Labeling. This is used as an assumption›
  qualified definition DISAMBIG :: "nat ⇒ bool" where
    "DISAMBIG n ≡ True"

  lemmas LABEL_simps = BIND_def CTXT_def HIER_def SPLIT_def VC_def

  lemma Initial_Label: "CTXT 0 [] outp P ⟹ P"
    by (simp add: Case_Labeling.CTXT_def)

  lemma
    BIND_I: "P ⟹ BIND name inp P" and
    BIND_D: "BIND name inp P ⟹ P" and
    VC_I: "P ⟹ VC ct P"
    unfolding Case_Labeling.BIND_def Case_Labeling.VC_def .
  
  lemma DISAMBIG_I: "(DISAMBIG n ⟹ P) ⟹ P"
    by (auto simp: DISAMBIG_def Case_Labeling.VC_def)

  lemma DISAMBIG_E: "(DISAMBIG n ⟹ P) ⟹ P"
    by (auto simp: DISAMBIG_def)

  text ‹Lemmas for the tuple postprocessing›
  lemma SPLIT_reflection: "SPLIT x y ⟹ (x ≡ y)"
    unfolding SPLIT_def by (rule eq_reflection)
  
  lemma rev_SPLIT_reflection: "(x ≡ y) ⟹ SPLIT x y"
    unfolding SPLIT_def ..
  
  lemma SPLIT_sym: "SPLIT x y ⟹ SPLIT y x"
    unfolding SPLIT_def by (rule sym)
  
  lemma SPLIT_thin_refl: "⟦SPLIT x x; PROP W⟧ ⟹ PROP W" .
  
  lemma SPLIT_subst: "⟦SPLIT x y; P x⟧ ⟹ P y"
    unfolding SPLIT_def by hypsubst
  
  lemma SPLIT_prodE:
    assumes "SPLIT (x1, y1) (x2, y2)"
    obtains "SPLIT x1 x2" "SPLIT y1 y2"
    using assms unfolding SPLIT_def by auto


end

text ‹
  The labeling constants were qualified to not interfere with any other theory.
  The following locale allows using a nice syntax in other theories 
›

locale Labeling_Syntax begin
  abbreviation VAR where "VAR ≡ Case_Labeling.VAR"
  abbreviation VC ("V⟨(2_,_:/ _)⟩") where "VC bl ct  ≡ Case_Labeling.VC (bl # ct)"
  abbreviation CTXT ("C⟨(2_,_,_:/ _⟩)") where "CTXT ≡ Case_Labeling.CTXT"
  abbreviation BIND ("B⟨(2_,_:/ _⟩)") where "BIND ≡ Case_Labeling.BIND"
  abbreviation HIER ("H⟨(2_:/ _⟩)") where "HIER ≡ Case_Labeling.HIER"
  abbreviation SPLIT where "SPLIT ≡ Case_Labeling.SPLIT"
end

text ‹Lemmas for converting terms from @{term Suc}/@{term "0::nat"} notation to numerals›
lemma Suc_numerals_conv:
  "Suc 0 = Numeral1"
  "Suc (numeral n) = numeral (n + num.One)"
  by auto

lemmas Suc_numeral_simps = Suc_numerals_conv add_num_simps


section ‹Casify›

text ‹
  Introduces a command @{verbatim print_nested_cases}. This is similar to @{verbatim print_cases},
  but shows also the nested cases.
›
ML_file "print_nested_cases.ML"

ML_file "util.ML"

text ‹Introduces the proof method.›
ML_file "casify.ML"


ML {*
  val casify_defs = Casify.Options { simp_all_cases=true, split_right_only=true, protect_subgoals=false }
*}

method_setup prepare_labels = {*
  Scan.succeed (fn ctxt => SIMPLE_METHOD (ALLGOALS (Casify.prepare_labels_tac ctxt)))
*} "VCG labelling: prepare labels"

method_setup casify = {* Casify.casify_method_setup casify_defs *}
  "VCG labelling: Turn the labels into cases"

end