<commit_before>(* 
    ID:         $Id$
    Author:     <NAME> and <NAME>, NICTA

  consequences of type definition theorems, 
  and of extended type definition theorems
*)

header {* Type Definition Theorems *}

theory TdThs
imports Main
begin

section "More lemmas about normal type definitions"

lemma
  tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
  tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
  tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
  by (auto simp: type_definition_def)

lemma td_nat_int: 
  "type_definition int nat (Collect (op <= 0))"
  unfolding type_definition_def by auto

context type_definition
begin

lemmas Rep' [iff] = Rep [simplified]  (* if A is given as Collect .. *)

declare Rep_inverse [simp] Rep_inject [simp]

lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
  by (simp add: Abs_inject)
   
lemma Abs_inverse': 
  "r : A ==> Abs r = a ==> Rep a = r"
  by (safe elim!: Abs_inverse)

lemma Rep_comp_inverse: 
  "Rep o f = g ==> Abs o g = f"
  using Rep_inverse by (auto intro: ext)

lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
  by simp

lemma Rep_inverse': "Rep a = r ==> Abs r = a"
  by (safe intro!: Rep_inverse)

lemma comp_Abs_inverse: 
  "f o Abs = g ==> g o Rep = f"
  using Rep_inverse by (auto intro: ext) 

lemma set_Rep: 
  "A = range Rep"
proof (rule set_ext)
  fix x
  show "(x \<in> A) = (x \<in> range Rep)"
    by (auto dest: Abs_inverse [of x, symmetric])
qed  

lemma set_Rep_Abs: "A = range (Rep o Abs)"
proof (rule set_ext)
  fix x
  show "(x \<in> A) = (x \<in> range (Rep o Abs))"
    by (auto dest: Abs_inverse [of x, symmetric])
qed  

lemma Abs_inj_on: "inj_on Abs A"
  unfolding inj_on_def 
  by (auto dest: Abs_inject [THEN iffD1])

lemma image: "Abs ` A = UNIV"
  by (auto intro!: image_eqI)

lemmas td_thm = type_definition_axioms

lemma fns1: 
  "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
  by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)

lemmas fns1a = disjI1 [THEN fns1]
lemmas fns1b = disjI2 [THEN fns1]

lemma fns4:
  "Rep o fa o Abs = fr ==> 
   Rep o fa = fr o Rep & fa o Abs = Abs o fr"
  by (auto intro!: ext)

end

interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
  by (rule td_nat_int)

-- "resetting to the default nat induct and cases rules"
declare Nat.induct [case_names 0 Suc, induct type]
declare Nat.exhaust [case_names 0 Suc, cases type]


subsection "Extended form of type definition predicate"

lemma td_conds:
  "norm o norm = norm ==> (fr o norm = norm o fr) = 
    (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
  apply safe
    apply (simp_all add: o_assoc [symmetric])
   apply (simp_all add: o_assoc)
  done

lemma fn_comm_power:<commit_msg>more robust declaration of nat_induct;<commit_after>(* 
    ID:         $Id$
    Author:     <NAME> and <NAME>, NICTA

  consequences of type definition theorems, 
  and of extended type definition theorems
*)

header {* Type Definition Theorems *}

theory TdThs
imports Main
begin

section "More lemmas about normal type definitions"

lemma
  tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
  tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
  tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
  by (auto simp: type_definition_def)

lemma td_nat_int: 
  "type_definition int nat (Collect (op <= 0))"
  unfolding type_definition_def by auto

context type_definition
begin

lemmas Rep' [iff] = Rep [simplified]  (* if A is given as Collect .. *)

declare Rep_inverse [simp] Rep_inject [simp]

lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
  by (simp add: Abs_inject)
   
lemma Abs_inverse': 
  "r : A ==> Abs r = a ==> Rep a = r"
  by (safe elim!: Abs_inverse)

lemma Rep_comp_inverse: 
  "Rep o f = g ==> Abs o g = f"
  using Rep_inverse by (auto intro: ext)

lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
  by simp

lemma Rep_inverse': "Rep a = r ==> Abs r = a"
  by (safe intro!: Rep_inverse)

lemma comp_Abs_inverse: 
  "f o Abs = g ==> g o Rep = f"
  using Rep_inverse by (auto intro: ext) 

lemma set_Rep: 
  "A = range Rep"
proof (rule set_ext)
  fix x
  show "(x \<in> A) = (x \<in> range Rep)"
    by (auto dest: Abs_inverse [of x, symmetric])
qed  

lemma set_Rep_Abs: "A = range (Rep o Abs)"
proof (rule set_ext)
  fix x
  show "(x \<in> A) = (x \<in> range (Rep o Abs))"
    by (auto dest: Abs_inverse [of x, symmetric])
qed  

lemma Abs_inj_on: "inj_on Abs A"
  unfolding inj_on_def 
  by (auto dest: Abs_inject [THEN iffD1])

lemma image: "Abs ` A = UNIV"
  by (auto intro!: image_eqI)

lemmas td_thm = type_definition_axioms

lemma fns1: 
  "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
  by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)

lemmas fns1a = disjI1 [THEN fns1]
lemmas fns1b = disjI2 [THEN fns1]

lemma fns4:
  "Rep o fa o Abs = fr ==> 
   Rep o fa = fr o Rep & fa o Abs = Abs o fr"
  by (auto intro!: ext)

end

interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
  by (rule td_nat_int)

text "resetting to the default nat induct and cases rules"
declare nat_induct [induct type: nat]
declare nat.exhaust [cases type: nat]


subsection "Extended form of type definition predicate"

lemma td_conds:
  "norm o norm = norm ==> (fr o norm = norm o fr) = 
    (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
  apply safe
    apply (simp_all add: o_assoc [symmetric])
   apply (simp_all add: o_assoc)
  done

lemma fn_comm_power:
{'fraction_non_alphanumeric': 0.11746307558644657, 'fraction_numerical': 0.005212858384013901, 'mean_word_length': 3.3343373493975905, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 61, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3270297', 'n_tokens_mistral': 2253, 'n_tokens_neox': 2154, 'n_words': 848}